↳ ITRS

  ↳ ITRStoIDPProof

z

Cond_eval1(TRUE, x, y, z) → eval(-@z(x, 1@z), y, z)
Cond_eval(TRUE, x, y, z) → eval(x, y, z)
Cond_eval2(TRUE, x, y, z) → eval(x, -@z(y, 1@z), z)
eval(x, y, z) → Cond_eval1(&&(&&(>@z(+@z(x, y), z), >=@z(z, 0@z)), >@z(x, 0@z)), x, y, z)
eval(x, y, z) → Cond_eval2(&&(&&(&&(>@z(+@z(x, y), z), >=@z(z, 0@z)), >=@z(0@z, x)), >@z(y, 0@z)), x, y, z)
eval(x, y, z) → Cond_eval(&&(&&(&&(>@z(+@z(x, y), z), >=@z(z, 0@z)), >=@z(0@z, x)), >=@z(0@z, y)), x, y, z)

Cond_eval1(TRUE, x0, x1, x2)
Cond_eval(TRUE, x0, x1, x2)
Cond_eval2(TRUE, x0, x1, x2)
eval(x0, x1, x2)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

z

Cond_eval1(TRUE, x, y, z) → eval(-@z(x, 1@z), y, z)
Cond_eval(TRUE, x, y, z) → eval(x, y, z)
Cond_eval2(TRUE, x, y, z) → eval(x, -@z(y, 1@z), z)
eval(x, y, z) → Cond_eval1(&&(&&(>@z(+@z(x, y), z), >=@z(z, 0@z)), >@z(x, 0@z)), x, y, z)
eval(x, y, z) → Cond_eval2(&&(&&(&&(>@z(+@z(x, y), z), >=@z(z, 0@z)), >=@z(0@z, x)), >@z(y, 0@z)), x, y, z)
eval(x, y, z) → Cond_eval(&&(&&(&&(>@z(+@z(x, y), z), >=@z(z, 0@z)), >=@z(0@z, x)), >=@z(0@z, y)), x, y, z)

(0) -> (1), if ((y[0] →^* y[1])∧(z[0] →^* z[1])∧(x[0] →^* x[1]))

(0) -> (2), if ((y[0] →^* y[2])∧(z[0] →^* z[2])∧(x[0] →^* x[2]))

(0) -> (3), if ((y[0] →^* y[3])∧(z[0] →^* z[3])∧(x[0] →^* x[3]))

(1) -> (5), if ((z[1] →^* z[5])∧(x[1] →^* x[5])∧(y[1] →^* y[5])∧(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)) →^* TRUE))

(2) -> (0), if ((z[2] →^* z[0])∧(x[2] →^* x[0])∧(y[2] →^* y[0])∧(&&(&&(&&(>@z(+@z(x[2], y[2]), z[2]), >=@z(z[2], 0@z)), >=@z(0@z, x[2])), >=@z(0@z, y[2])) →^* TRUE))

(3) -> (4), if ((z[3] →^* z[4])∧(x[3] →^* x[4])∧(y[3] →^* y[4])∧(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)) →^* TRUE))

(4) -> (1), if ((-@z(y[4], 1@z) →^* y[1])∧(z[4] →^* z[1])∧(x[4] →^* x[1]))

(4) -> (2), if ((-@z(y[4], 1@z) →^* y[2])∧(z[4] →^* z[2])∧(x[4] →^* x[2]))

(4) -> (3), if ((-@z(y[4], 1@z) →^* y[3])∧(z[4] →^* z[3])∧(x[4] →^* x[3]))

(5) -> (1), if ((y[5] →^* y[1])∧(z[5] →^* z[1])∧(-@z(x[5], 1@z) →^* x[1]))

(5) -> (2), if ((y[5] →^* y[2])∧(z[5] →^* z[2])∧(-@z(x[5], 1@z) →^* x[2]))

(5) -> (3), if ((y[5] →^* y[3])∧(z[5] →^* z[3])∧(-@z(x[5], 1@z) →^* x[3]))

Cond_eval1(TRUE, x0, x1, x2)
Cond_eval(TRUE, x0, x1, x2)
Cond_eval2(TRUE, x0, x1, x2)
eval(x0, x1, x2)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDPNonInfProof

z

(0) -> (1), if ((y[0] →^* y[1])∧(z[0] →^* z[1])∧(x[0] →^* x[1]))

(0) -> (2), if ((y[0] →^* y[2])∧(z[0] →^* z[2])∧(x[0] →^* x[2]))

(0) -> (3), if ((y[0] →^* y[3])∧(z[0] →^* z[3])∧(x[0] →^* x[3]))

(1) -> (5), if ((z[1] →^* z[5])∧(x[1] →^* x[5])∧(y[1] →^* y[5])∧(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)) →^* TRUE))

(2) -> (0), if ((z[2] →^* z[0])∧(x[2] →^* x[0])∧(y[2] →^* y[0])∧(&&(&&(&&(>@z(+@z(x[2], y[2]), z[2]), >=@z(z[2], 0@z)), >=@z(0@z, x[2])), >=@z(0@z, y[2])) →^* TRUE))

(3) -> (4), if ((z[3] →^* z[4])∧(x[3] →^* x[4])∧(y[3] →^* y[4])∧(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)) →^* TRUE))

(4) -> (1), if ((-@z(y[4], 1@z) →^* y[1])∧(z[4] →^* z[1])∧(x[4] →^* x[1]))

(4) -> (2), if ((-@z(y[4], 1@z) →^* y[2])∧(z[4] →^* z[2])∧(x[4] →^* x[2]))

(4) -> (3), if ((-@z(y[4], 1@z) →^* y[3])∧(z[4] →^* z[3])∧(x[4] →^* x[3]))

(5) -> (1), if ((y[5] →^* y[1])∧(z[5] →^* z[1])∧(-@z(x[5], 1@z) →^* x[1]))

(5) -> (2), if ((y[5] →^* y[2])∧(z[5] →^* z[2])∧(-@z(x[5], 1@z) →^* x[2]))

(5) -> (3), if ((y[5] →^* y[3])∧(z[5] →^* z[3])∧(-@z(x[5], 1@z) →^* x[3]))

Cond_eval1(TRUE, x0, x1, x2)
Cond_eval(TRUE, x0, x1, x2)
Cond_eval2(TRUE, x0, x1, x2)
eval(x0, x1, x2)

• We consider the chain EVAL(x[2], y[2], z[2]) → COND_EVAL(&&(&&(&&(>@z(+@z(x[2], y[2]), z[2]), >=@z(z[2], 0@z)), >=@z(0@z, x[2])), >=@z(0@z, y[2])), x[2], y[2], z[2]), COND_EVAL(TRUE, x[0], y[0], z[0]) → EVAL(x[0], y[0], z[0]), EVAL(x[2], y[2], z[2]) → COND_EVAL(&&(&&(&&(>@z(+@z(x[2], y[2]), z[2]), >=@z(z[2], 0@z)), >=@z(0@z, x[2])), >=@z(0@z, y[2])), x[2], y[2], z[2]) which results in the following constraint:
  

  (1)    (z[2]=z[0]∧z[0]=z[2]1∧x[2]=x[0]∧y[0]=y[2]1∧y[2]=y[0]∧x[0]=x[2]1∧&&(&&(&&(>@z(+@z(x[2], y[2]), z[2]), >=@z(z[2], 0@z)), >=@z(0@z, x[2])), >=@z(0@z, y[2]))=TRUE ⇒ COND_EVAL(TRUE, x[0], y[0], z[0])≥NonInfC∧COND_EVAL(TRUE, x[0], y[0], z[0])≥EVAL(x[0], y[0], z[0])∧(U^Increasing(EVAL(x[0], y[0], z[0])), ≥))

  
  
  We simplified constraint (1) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (2)    (>=@z(0@z, y[2])=TRUE∧>=@z(0@z, x[2])=TRUE∧>@z(+@z(x[2], y[2]), z[2])=TRUE∧>=@z(z[2], 0@z)=TRUE ⇒ COND_EVAL(TRUE, x[2], y[2], z[2])≥NonInfC∧COND_EVAL(TRUE, x[2], y[2], z[2])≥EVAL(x[2], y[2], z[2])∧(U^Increasing(EVAL(x[0], y[0], z[0])), ≥))

  
  
  We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (3)    ((-1)y[2] ≥ 0∧(-1)x[2] ≥ 0∧-1 + x[2] + y[2] + (-1)z[2] ≥ 0∧z[2] ≥ 0 ⇒ (U^Increasing(EVAL(x[0], y[0], z[0])), ≥)∧(-1)Bound + (-1)z[2] ≥ 0∧-1 ≥ 0)

  
  
  We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (4)    ((-1)y[2] ≥ 0∧(-1)x[2] ≥ 0∧-1 + x[2] + y[2] + (-1)z[2] ≥ 0∧z[2] ≥ 0 ⇒ (U^Increasing(EVAL(x[0], y[0], z[0])), ≥)∧(-1)Bound + (-1)z[2] ≥ 0∧-1 ≥ 0)

  
  
  We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (5)    ((-1)x[2] ≥ 0∧(-1)y[2] ≥ 0∧-1 + x[2] + y[2] + (-1)z[2] ≥ 0∧z[2] ≥ 0 ⇒ (U^Increasing(EVAL(x[0], y[0], z[0])), ≥)∧(-1)Bound + (-1)z[2] ≥ 0∧-1 ≥ 0)

  
  
  We solved constraint (5) using rule (IDP_SMT_SPLIT).
• We consider the chain EVAL(x[2], y[2], z[2]) → COND_EVAL(&&(&&(&&(>@z(+@z(x[2], y[2]), z[2]), >=@z(z[2], 0@z)), >=@z(0@z, x[2])), >=@z(0@z, y[2])), x[2], y[2], z[2]), COND_EVAL(TRUE, x[0], y[0], z[0]) → EVAL(x[0], y[0], z[0]), EVAL(x[3], y[3], z[3]) → COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3]) which results in the following constraint:
  

  (6)    (y[0]=y[3]∧z[2]=z[0]∧x[2]=x[0]∧x[0]=x[3]∧y[2]=y[0]∧z[0]=z[3]∧&&(&&(&&(>@z(+@z(x[2], y[2]), z[2]), >=@z(z[2], 0@z)), >=@z(0@z, x[2])), >=@z(0@z, y[2]))=TRUE ⇒ COND_EVAL(TRUE, x[0], y[0], z[0])≥NonInfC∧COND_EVAL(TRUE, x[0], y[0], z[0])≥EVAL(x[0], y[0], z[0])∧(U^Increasing(EVAL(x[0], y[0], z[0])), ≥))

  
  
  We simplified constraint (6) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (7)    (>=@z(0@z, y[2])=TRUE∧>=@z(0@z, x[2])=TRUE∧>@z(+@z(x[2], y[2]), z[2])=TRUE∧>=@z(z[2], 0@z)=TRUE ⇒ COND_EVAL(TRUE, x[2], y[2], z[2])≥NonInfC∧COND_EVAL(TRUE, x[2], y[2], z[2])≥EVAL(x[2], y[2], z[2])∧(U^Increasing(EVAL(x[0], y[0], z[0])), ≥))

  
  
  We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (8)    ((-1)y[2] ≥ 0∧(-1)x[2] ≥ 0∧-1 + x[2] + y[2] + (-1)z[2] ≥ 0∧z[2] ≥ 0 ⇒ (U^Increasing(EVAL(x[0], y[0], z[0])), ≥)∧(-1)Bound + (-1)z[2] ≥ 0∧-1 ≥ 0)

  
  
  We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (9)    ((-1)y[2] ≥ 0∧(-1)x[2] ≥ 0∧-1 + x[2] + y[2] + (-1)z[2] ≥ 0∧z[2] ≥ 0 ⇒ (U^Increasing(EVAL(x[0], y[0], z[0])), ≥)∧(-1)Bound + (-1)z[2] ≥ 0∧-1 ≥ 0)

  
  
  We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (10)    ((-1)x[2] ≥ 0∧-1 + x[2] + y[2] + (-1)z[2] ≥ 0∧(-1)y[2] ≥ 0∧z[2] ≥ 0 ⇒ (U^Increasing(EVAL(x[0], y[0], z[0])), ≥)∧-1 ≥ 0∧(-1)Bound + (-1)z[2] ≥ 0)

  
  
  We solved constraint (10) using rule (IDP_SMT_SPLIT).
• We consider the chain EVAL(x[2], y[2], z[2]) → COND_EVAL(&&(&&(&&(>@z(+@z(x[2], y[2]), z[2]), >=@z(z[2], 0@z)), >=@z(0@z, x[2])), >=@z(0@z, y[2])), x[2], y[2], z[2]), COND_EVAL(TRUE, x[0], y[0], z[0]) → EVAL(x[0], y[0], z[0]), EVAL(x[1], y[1], z[1]) → COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1]) which results in the following constraint:
  

  (11)    (z[2]=z[0]∧x[2]=x[0]∧y[2]=y[0]∧y[0]=y[1]∧x[0]=x[1]∧z[0]=z[1]∧&&(&&(&&(>@z(+@z(x[2], y[2]), z[2]), >=@z(z[2], 0@z)), >=@z(0@z, x[2])), >=@z(0@z, y[2]))=TRUE ⇒ COND_EVAL(TRUE, x[0], y[0], z[0])≥NonInfC∧COND_EVAL(TRUE, x[0], y[0], z[0])≥EVAL(x[0], y[0], z[0])∧(U^Increasing(EVAL(x[0], y[0], z[0])), ≥))

  
  
  We simplified constraint (11) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (12)    (>=@z(0@z, y[2])=TRUE∧>=@z(0@z, x[2])=TRUE∧>@z(+@z(x[2], y[2]), z[2])=TRUE∧>=@z(z[2], 0@z)=TRUE ⇒ COND_EVAL(TRUE, x[2], y[2], z[2])≥NonInfC∧COND_EVAL(TRUE, x[2], y[2], z[2])≥EVAL(x[2], y[2], z[2])∧(U^Increasing(EVAL(x[0], y[0], z[0])), ≥))

  
  
  We simplified constraint (12) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (13)    ((-1)y[2] ≥ 0∧(-1)x[2] ≥ 0∧-1 + x[2] + y[2] + (-1)z[2] ≥ 0∧z[2] ≥ 0 ⇒ (U^Increasing(EVAL(x[0], y[0], z[0])), ≥)∧(-1)Bound + (-1)z[2] ≥ 0∧-1 ≥ 0)

  
  
  We simplified constraint (13) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (14)    ((-1)y[2] ≥ 0∧(-1)x[2] ≥ 0∧-1 + x[2] + y[2] + (-1)z[2] ≥ 0∧z[2] ≥ 0 ⇒ (U^Increasing(EVAL(x[0], y[0], z[0])), ≥)∧(-1)Bound + (-1)z[2] ≥ 0∧-1 ≥ 0)

  
  
  We simplified constraint (14) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (15)    ((-1)y[2] ≥ 0∧(-1)x[2] ≥ 0∧z[2] ≥ 0∧-1 + x[2] + y[2] + (-1)z[2] ≥ 0 ⇒ (U^Increasing(EVAL(x[0], y[0], z[0])), ≥)∧(-1)Bound + (-1)z[2] ≥ 0∧-1 ≥ 0)

  
  
  We solved constraint (15) using rule (IDP_SMT_SPLIT).

• We consider the chain EVAL(x[1], y[1], z[1]) → COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1]) which results in the following constraint:
  

  (16)    (EVAL(x[1], y[1], z[1])≥NonInfC∧EVAL(x[1], y[1], z[1])≥COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1])∧(U^Increasing(COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1])), ≥))

  
  
  We simplified constraint (16) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (17)    ((U^Increasing(COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (17) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (18)    ((U^Increasing(COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (18) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (19)    (0 ≥ 0∧0 ≥ 0∧(U^Increasing(COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1])), ≥))

  
  
  We simplified constraint (19) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (20)    (0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 ≥ 0∧0 ≥ 0∧(U^Increasing(COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1])), ≥)∧0 = 0)

  
  
  

• We consider the chain EVAL(x[2], y[2], z[2]) → COND_EVAL(&&(&&(&&(>@z(+@z(x[2], y[2]), z[2]), >=@z(z[2], 0@z)), >=@z(0@z, x[2])), >=@z(0@z, y[2])), x[2], y[2], z[2]) which results in the following constraint:
  

  (21)    (EVAL(x[2], y[2], z[2])≥NonInfC∧EVAL(x[2], y[2], z[2])≥COND_EVAL(&&(&&(&&(>@z(+@z(x[2], y[2]), z[2]), >=@z(z[2], 0@z)), >=@z(0@z, x[2])), >=@z(0@z, y[2])), x[2], y[2], z[2])∧(U^Increasing(COND_EVAL(&&(&&(&&(>@z(+@z(x[2], y[2]), z[2]), >=@z(z[2], 0@z)), >=@z(0@z, x[2])), >=@z(0@z, y[2])), x[2], y[2], z[2])), ≥))

  
  
  We simplified constraint (21) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (22)    ((U^Increasing(COND_EVAL(&&(&&(&&(>@z(+@z(x[2], y[2]), z[2]), >=@z(z[2], 0@z)), >=@z(0@z, x[2])), >=@z(0@z, y[2])), x[2], y[2], z[2])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (22) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (23)    ((U^Increasing(COND_EVAL(&&(&&(&&(>@z(+@z(x[2], y[2]), z[2]), >=@z(z[2], 0@z)), >=@z(0@z, x[2])), >=@z(0@z, y[2])), x[2], y[2], z[2])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (23) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (24)    ((U^Increasing(COND_EVAL(&&(&&(&&(>@z(+@z(x[2], y[2]), z[2]), >=@z(z[2], 0@z)), >=@z(0@z, x[2])), >=@z(0@z, y[2])), x[2], y[2], z[2])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (24) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (25)    (0 = 0∧(U^Increasing(COND_EVAL(&&(&&(&&(>@z(+@z(x[2], y[2]), z[2]), >=@z(z[2], 0@z)), >=@z(0@z, x[2])), >=@z(0@z, y[2])), x[2], y[2], z[2])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0)

  
  
  

• We consider the chain EVAL(x[3], y[3], z[3]) → COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3]) which results in the following constraint:
  

  (26)    (EVAL(x[3], y[3], z[3])≥NonInfC∧EVAL(x[3], y[3], z[3])≥COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])∧(U^Increasing(COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥))

  
  
  We simplified constraint (26) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (27)    ((U^Increasing(COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (27) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (28)    ((U^Increasing(COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (28) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (29)    ((U^Increasing(COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (29) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (30)    (0 = 0∧0 ≥ 0∧(U^Increasing(COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥)∧0 = 0∧0 = 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0)

  
  
  

• We consider the chain EVAL(x[3], y[3], z[3]) → COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3]), COND_EVAL2(TRUE, x[4], y[4], z[4]) → EVAL(x[4], -@z(y[4], 1@z), z[4]), EVAL(x[3], y[3], z[3]) → COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3]) which results in the following constraint:
  

  (31)    (z[4]=z[3]1∧z[3]=z[4]∧-@z(y[4], 1@z)=y[3]1∧&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z))=TRUE∧y[3]=y[4]∧x[3]=x[4]∧x[4]=x[3]1 ⇒ COND_EVAL2(TRUE, x[4], y[4], z[4])≥NonInfC∧COND_EVAL2(TRUE, x[4], y[4], z[4])≥EVAL(x[4], -@z(y[4], 1@z), z[4])∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥))

  
  
  We simplified constraint (31) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (32)    (>@z(y[3], 0@z)=TRUE∧>=@z(0@z, x[3])=TRUE∧>@z(+@z(x[3], y[3]), z[3])=TRUE∧>=@z(z[3], 0@z)=TRUE ⇒ COND_EVAL2(TRUE, x[3], y[3], z[3])≥NonInfC∧COND_EVAL2(TRUE, x[3], y[3], z[3])≥EVAL(x[3], -@z(y[3], 1@z), z[3])∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥))

  
  
  We simplified constraint (32) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (33)    (-1 + y[3] ≥ 0∧(-1)x[3] ≥ 0∧-1 + x[3] + y[3] + (-1)z[3] ≥ 0∧z[3] ≥ 0 ⇒ (U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (33) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (34)    (-1 + y[3] ≥ 0∧(-1)x[3] ≥ 0∧-1 + x[3] + y[3] + (-1)z[3] ≥ 0∧z[3] ≥ 0 ⇒ (U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (34) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (35)    (-1 + x[3] + y[3] + (-1)z[3] ≥ 0∧(-1)x[3] ≥ 0∧z[3] ≥ 0∧-1 + y[3] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥)∧0 ≥ 0)

  
  
  We simplified constraint (35) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (36)    (-1 + (-1)x[3] + y[3] + (-1)z[3] ≥ 0∧x[3] ≥ 0∧z[3] ≥ 0∧-1 + y[3] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥)∧0 ≥ 0)

  
  
  We simplified constraint (36) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (37)    (y[3] ≥ 0∧x[3] ≥ 0∧z[3] ≥ 0∧x[3] + z[3] + y[3] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥)∧0 ≥ 0)

  
  
  
• We consider the chain EVAL(x[3], y[3], z[3]) → COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3]), COND_EVAL2(TRUE, x[4], y[4], z[4]) → EVAL(x[4], -@z(y[4], 1@z), z[4]), EVAL(x[1], y[1], z[1]) → COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1]) which results in the following constraint:
  

  (38)    (z[3]=z[4]∧&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z))=TRUE∧y[3]=y[4]∧z[4]=z[1]∧x[3]=x[4]∧-@z(y[4], 1@z)=y[1]∧x[4]=x[1] ⇒ COND_EVAL2(TRUE, x[4], y[4], z[4])≥NonInfC∧COND_EVAL2(TRUE, x[4], y[4], z[4])≥EVAL(x[4], -@z(y[4], 1@z), z[4])∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥))

  
  
  We simplified constraint (38) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (39)    (>@z(y[3], 0@z)=TRUE∧>=@z(0@z, x[3])=TRUE∧>@z(+@z(x[3], y[3]), z[3])=TRUE∧>=@z(z[3], 0@z)=TRUE ⇒ COND_EVAL2(TRUE, x[3], y[3], z[3])≥NonInfC∧COND_EVAL2(TRUE, x[3], y[3], z[3])≥EVAL(x[3], -@z(y[3], 1@z), z[3])∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥))

  
  
  We simplified constraint (39) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (40)    (-1 + y[3] ≥ 0∧(-1)x[3] ≥ 0∧-1 + x[3] + y[3] + (-1)z[3] ≥ 0∧z[3] ≥ 0 ⇒ (U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (40) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (41)    (-1 + y[3] ≥ 0∧(-1)x[3] ≥ 0∧-1 + x[3] + y[3] + (-1)z[3] ≥ 0∧z[3] ≥ 0 ⇒ (U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (41) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (42)    ((-1)x[3] ≥ 0∧-1 + y[3] ≥ 0∧z[3] ≥ 0∧-1 + x[3] + y[3] + (-1)z[3] ≥ 0 ⇒ (U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (42) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (43)    (x[3] ≥ 0∧-1 + y[3] ≥ 0∧z[3] ≥ 0∧-1 + (-1)x[3] + y[3] + (-1)z[3] ≥ 0 ⇒ (U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (43) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (44)    (x[3] ≥ 0∧y[3] ≥ 0∧z[3] ≥ 0∧(-1)x[3] + y[3] + (-1)z[3] ≥ 0 ⇒ (U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (44) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (45)    (x[3] ≥ 0∧x[3] + z[3] + y[3] ≥ 0∧z[3] ≥ 0∧y[3] ≥ 0 ⇒ (U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  
• We consider the chain EVAL(x[3], y[3], z[3]) → COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3]), COND_EVAL2(TRUE, x[4], y[4], z[4]) → EVAL(x[4], -@z(y[4], 1@z), z[4]), EVAL(x[2], y[2], z[2]) → COND_EVAL(&&(&&(&&(>@z(+@z(x[2], y[2]), z[2]), >=@z(z[2], 0@z)), >=@z(0@z, x[2])), >=@z(0@z, y[2])), x[2], y[2], z[2]) which results in the following constraint:
  

  (46)    (z[4]=z[2]∧z[3]=z[4]∧&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z))=TRUE∧y[3]=y[4]∧x[3]=x[4]∧-@z(y[4], 1@z)=y[2]∧x[4]=x[2] ⇒ COND_EVAL2(TRUE, x[4], y[4], z[4])≥NonInfC∧COND_EVAL2(TRUE, x[4], y[4], z[4])≥EVAL(x[4], -@z(y[4], 1@z), z[4])∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥))

  
  
  We simplified constraint (46) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (47)    (>@z(y[3], 0@z)=TRUE∧>=@z(0@z, x[3])=TRUE∧>@z(+@z(x[3], y[3]), z[3])=TRUE∧>=@z(z[3], 0@z)=TRUE ⇒ COND_EVAL2(TRUE, x[3], y[3], z[3])≥NonInfC∧COND_EVAL2(TRUE, x[3], y[3], z[3])≥EVAL(x[3], -@z(y[3], 1@z), z[3])∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥))

  
  
  We simplified constraint (47) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (48)    (-1 + y[3] ≥ 0∧(-1)x[3] ≥ 0∧-1 + x[3] + y[3] + (-1)z[3] ≥ 0∧z[3] ≥ 0 ⇒ (U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (48) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (49)    (-1 + y[3] ≥ 0∧(-1)x[3] ≥ 0∧-1 + x[3] + y[3] + (-1)z[3] ≥ 0∧z[3] ≥ 0 ⇒ (U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (49) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (50)    (z[3] ≥ 0∧(-1)x[3] ≥ 0∧-1 + y[3] ≥ 0∧-1 + x[3] + y[3] + (-1)z[3] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥))

  
  
  We simplified constraint (50) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (51)    (z[3] ≥ 0∧x[3] ≥ 0∧-1 + y[3] ≥ 0∧-1 + (-1)x[3] + y[3] + (-1)z[3] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥))

  
  
  We simplified constraint (51) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (52)    (z[3] ≥ 0∧x[3] ≥ 0∧y[3] ≥ 0∧(-1)x[3] + y[3] + (-1)z[3] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥))

  
  
  We simplified constraint (52) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (53)    (z[3] ≥ 0∧x[3] ≥ 0∧x[3] + z[3] + y[3] ≥ 0∧y[3] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥))

  
  
  

• We consider the chain EVAL(x[1], y[1], z[1]) → COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1]), COND_EVAL1(TRUE, x[5], y[5], z[5]) → EVAL(-@z(x[5], 1@z), y[5], z[5]), EVAL(x[1], y[1], z[1]) → COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1]) which results in the following constraint:
  

  (54)    (z[5]=z[1]1∧z[1]=z[5]∧y[5]=y[1]1∧&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z))=TRUE∧-@z(x[5], 1@z)=x[1]1∧x[1]=x[5]∧y[1]=y[5] ⇒ COND_EVAL1(TRUE, x[5], y[5], z[5])≥NonInfC∧COND_EVAL1(TRUE, x[5], y[5], z[5])≥EVAL(-@z(x[5], 1@z), y[5], z[5])∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥))

  
  
  We simplified constraint (54) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (55)    (>@z(x[1], 0@z)=TRUE∧>@z(+@z(x[1], y[1]), z[1])=TRUE∧>=@z(z[1], 0@z)=TRUE ⇒ COND_EVAL1(TRUE, x[1], y[1], z[1])≥NonInfC∧COND_EVAL1(TRUE, x[1], y[1], z[1])≥EVAL(-@z(x[1], 1@z), y[1], z[1])∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥))

  
  
  We simplified constraint (55) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (56)    (x[1] + -1 ≥ 0∧x[1] + -1 + y[1] + (-1)z[1] ≥ 0∧z[1] ≥ 0 ⇒ (U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (56) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (57)    (x[1] + -1 ≥ 0∧x[1] + -1 + y[1] + (-1)z[1] ≥ 0∧z[1] ≥ 0 ⇒ (U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (57) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (58)    (x[1] + -1 ≥ 0∧z[1] ≥ 0∧x[1] + -1 + y[1] + (-1)z[1] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0)

  
  
  We simplified constraint (58) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (59)    ((-1)y[1] + z[1] + x[1] ≥ 0∧z[1] ≥ 0∧x[1] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0)

  
  
  We simplified constraint (59) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (60)    (y[1] + z[1] + x[1] ≥ 0∧z[1] ≥ 0∧x[1] ≥ 0∧y[1] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0)

  
  

  (61)    ((-1)y[1] + z[1] + x[1] ≥ 0∧z[1] ≥ 0∧x[1] ≥ 0∧y[1] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0)

  
  
  
• We consider the chain EVAL(x[1], y[1], z[1]) → COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1]), COND_EVAL1(TRUE, x[5], y[5], z[5]) → EVAL(-@z(x[5], 1@z), y[5], z[5]), EVAL(x[2], y[2], z[2]) → COND_EVAL(&&(&&(&&(>@z(+@z(x[2], y[2]), z[2]), >=@z(z[2], 0@z)), >=@z(0@z, x[2])), >=@z(0@z, y[2])), x[2], y[2], z[2]) which results in the following constraint:
  

  (62)    (-@z(x[5], 1@z)=x[2]∧z[5]=z[2]∧z[1]=z[5]∧&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z))=TRUE∧y[5]=y[2]∧x[1]=x[5]∧y[1]=y[5] ⇒ COND_EVAL1(TRUE, x[5], y[5], z[5])≥NonInfC∧COND_EVAL1(TRUE, x[5], y[5], z[5])≥EVAL(-@z(x[5], 1@z), y[5], z[5])∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥))

  
  
  We simplified constraint (62) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (63)    (>@z(x[1], 0@z)=TRUE∧>@z(+@z(x[1], y[1]), z[1])=TRUE∧>=@z(z[1], 0@z)=TRUE ⇒ COND_EVAL1(TRUE, x[1], y[1], z[1])≥NonInfC∧COND_EVAL1(TRUE, x[1], y[1], z[1])≥EVAL(-@z(x[1], 1@z), y[1], z[1])∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥))

  
  
  We simplified constraint (63) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (64)    (x[1] + -1 ≥ 0∧x[1] + -1 + y[1] + (-1)z[1] ≥ 0∧z[1] ≥ 0 ⇒ (U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (64) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (65)    (x[1] + -1 ≥ 0∧x[1] + -1 + y[1] + (-1)z[1] ≥ 0∧z[1] ≥ 0 ⇒ (U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (65) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (66)    (z[1] ≥ 0∧x[1] + -1 + y[1] + (-1)z[1] ≥ 0∧x[1] + -1 ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0)

  
  
  We simplified constraint (66) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (67)    (z[1] ≥ 0∧x[1] ≥ 0∧(-1)y[1] + z[1] + x[1] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0)

  
  
  We simplified constraint (67) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (68)    (z[1] ≥ 0∧x[1] ≥ 0∧(-1)y[1] + z[1] + x[1] ≥ 0∧y[1] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0)

  
  

  (69)    (z[1] ≥ 0∧x[1] ≥ 0∧y[1] + z[1] + x[1] ≥ 0∧y[1] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0)

  
  
  
• We consider the chain EVAL(x[1], y[1], z[1]) → COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1]), COND_EVAL1(TRUE, x[5], y[5], z[5]) → EVAL(-@z(x[5], 1@z), y[5], z[5]), EVAL(x[3], y[3], z[3]) → COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3]) which results in the following constraint:
  

  (70)    (-@z(x[5], 1@z)=x[3]∧y[5]=y[3]∧z[1]=z[5]∧z[5]=z[3]∧&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z))=TRUE∧x[1]=x[5]∧y[1]=y[5] ⇒ COND_EVAL1(TRUE, x[5], y[5], z[5])≥NonInfC∧COND_EVAL1(TRUE, x[5], y[5], z[5])≥EVAL(-@z(x[5], 1@z), y[5], z[5])∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥))

  
  
  We simplified constraint (70) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (71)    (>@z(x[1], 0@z)=TRUE∧>@z(+@z(x[1], y[1]), z[1])=TRUE∧>=@z(z[1], 0@z)=TRUE ⇒ COND_EVAL1(TRUE, x[1], y[1], z[1])≥NonInfC∧COND_EVAL1(TRUE, x[1], y[1], z[1])≥EVAL(-@z(x[1], 1@z), y[1], z[1])∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥))

  
  
  We simplified constraint (71) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (72)    (x[1] + -1 ≥ 0∧x[1] + -1 + y[1] + (-1)z[1] ≥ 0∧z[1] ≥ 0 ⇒ (U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (72) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (73)    (x[1] + -1 ≥ 0∧x[1] + -1 + y[1] + (-1)z[1] ≥ 0∧z[1] ≥ 0 ⇒ (U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (73) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (74)    (z[1] ≥ 0∧x[1] + -1 ≥ 0∧x[1] + -1 + y[1] + (-1)z[1] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0)

  
  
  We simplified constraint (74) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (75)    (z[1] ≥ 0∧x[1] ≥ 0∧x[1] + y[1] + (-1)z[1] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0)

  
  
  We simplified constraint (75) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (76)    (z[1] ≥ 0∧x[1] ≥ 0∧x[1] + y[1] + (-1)z[1] ≥ 0∧y[1] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0)

  
  

  (77)    (z[1] ≥ 0∧x[1] ≥ 0∧x[1] + (-1)y[1] + (-1)z[1] ≥ 0∧y[1] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0)

  
  
  We simplified constraint (77) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (78)    (z[1] ≥ 0∧y[1] + z[1] + x[1] ≥ 0∧x[1] ≥ 0∧y[1] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0)

  
  
  

• COND_EVAL(TRUE, x, y, z) → EVAL(x, y, z)
  
  
• EVAL(x, y, z) → COND_EVAL1(&&(&&(>@z(+@z(x, y), z), >=@z(z, 0@z)), >@z(x, 0@z)), x, y, z)
  
  • (0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 ≥ 0∧0 ≥ 0∧(U^Increasing(COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1])), ≥)∧0 = 0)
    
  
  
• EVAL(x, y, z) → COND_EVAL(&&(&&(&&(>@z(+@z(x, y), z), >=@z(z, 0@z)), >=@z(0@z, x)), >=@z(0@z, y)), x, y, z)
  
  • (0 = 0∧(U^Increasing(COND_EVAL(&&(&&(&&(>@z(+@z(x[2], y[2]), z[2]), >=@z(z[2], 0@z)), >=@z(0@z, x[2])), >=@z(0@z, y[2])), x[2], y[2], z[2])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0)
    
  
  
• EVAL(x, y, z) → COND_EVAL2(&&(&&(&&(>@z(+@z(x, y), z), >=@z(z, 0@z)), >=@z(0@z, x)), >@z(y, 0@z)), x, y, z)
  
  • (0 = 0∧0 ≥ 0∧(U^Increasing(COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥)∧0 = 0∧0 = 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0)
    
  
  
• COND_EVAL2(TRUE, x, y, z) → EVAL(x, -@z(y, 1@z), z)
  
  • (y[3] ≥ 0∧x[3] ≥ 0∧z[3] ≥ 0∧x[3] + z[3] + y[3] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥)∧0 ≥ 0)
    
  • (x[3] ≥ 0∧x[3] + z[3] + y[3] ≥ 0∧z[3] ≥ 0∧y[3] ≥ 0 ⇒ (U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥)∧0 ≥ 0∧0 ≥ 0)
    
  • (z[3] ≥ 0∧x[3] ≥ 0∧x[3] + z[3] + y[3] ≥ 0∧y[3] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥))
    
  
  
• COND_EVAL1(TRUE, x, y, z) → EVAL(-@z(x, 1@z), y, z)
  
  • (y[1] + z[1] + x[1] ≥ 0∧z[1] ≥ 0∧x[1] ≥ 0∧y[1] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0)
    
  • ((-1)y[1] + z[1] + x[1] ≥ 0∧z[1] ≥ 0∧x[1] ≥ 0∧y[1] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0)
    
  • (z[1] ≥ 0∧x[1] ≥ 0∧(-1)y[1] + z[1] + x[1] ≥ 0∧y[1] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0)
    
  • (z[1] ≥ 0∧x[1] ≥ 0∧y[1] + z[1] + x[1] ≥ 0∧y[1] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0)
    
  • (z[1] ≥ 0∧x[1] ≥ 0∧x[1] + y[1] + (-1)z[1] ≥ 0∧y[1] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0)
    
  • (z[1] ≥ 0∧y[1] + z[1] + x[1] ≥ 0∧x[1] ≥ 0∧y[1] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0)
    
  
  

POL(-@z(x₁, x₂)) = x₁ + (-1)x₂   
POL(COND_EVAL2(x₁, x₂, x₃, x₄)) = -1 + (-1)x₄ + (-1)x₁   
POL(0@z) = 0   
POL(TRUE) = -1   
POL(&&(x₁, x₂)) = -1   
POL(EVAL(x₁, x₂, x₃)) = (-1)x₃   
POL(FALSE) = -1   
POL(>@z(x₁, x₂)) = -1   
POL(>=@z(x₁, x₂)) = -1   
POL(COND_EVAL1(x₁, x₂, x₃, x₄)) = -1 + (-1)x₄ + (-1)x₁   
POL(+@z(x₁, x₂)) = x₁ + x₂   
POL(COND_EVAL(x₁, x₂, x₃, x₄)) = -1 + (-1)x₄ + (-1)x₁   
POL(1@z) = 1   
POL(undefined) = -1   

COND_EVAL(TRUE, x[0], y[0], z[0]) → EVAL(x[0], y[0], z[0])

COND_EVAL(TRUE, x[0], y[0], z[0]) → EVAL(x[0], y[0], z[0])

EVAL(x[1], y[1], z[1]) → COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1])
EVAL(x[2], y[2], z[2]) → COND_EVAL(&&(&&(&&(>@z(+@z(x[2], y[2]), z[2]), >=@z(z[2], 0@z)), >=@z(0@z, x[2])), >=@z(0@z, y[2])), x[2], y[2], z[2])
EVAL(x[3], y[3], z[3]) → COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])
COND_EVAL2(TRUE, x[4], y[4], z[4]) → EVAL(x[4], -@z(y[4], 1@z), z[4])
COND_EVAL1(TRUE, x[5], y[5], z[5]) → EVAL(-@z(x[5], 1@z), y[5], z[5])

FALSE¹ → &&(FALSE, FALSE)¹
-@z¹ ↔
TRUE¹ → &&(TRUE, TRUE)¹
&&(TRUE, FALSE)¹ ↔ FALSE¹
&&(FALSE, TRUE)¹ ↔ FALSE¹

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDPNonInfProof

            ↳ IDP

              ↳ IDependencyGraphProof

z

(1) -> (5), if ((z[1] →^* z[5])∧(x[1] →^* x[5])∧(y[1] →^* y[5])∧(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)) →^* TRUE))

(4) -> (2), if ((-@z(y[4], 1@z) →^* y[2])∧(z[4] →^* z[2])∧(x[4] →^* x[2]))

(4) -> (3), if ((-@z(y[4], 1@z) →^* y[3])∧(z[4] →^* z[3])∧(x[4] →^* x[3]))

(5) -> (2), if ((y[5] →^* y[2])∧(z[5] →^* z[2])∧(-@z(x[5], 1@z) →^* x[2]))

(5) -> (3), if ((y[5] →^* y[3])∧(z[5] →^* z[3])∧(-@z(x[5], 1@z) →^* x[3]))

(3) -> (4), if ((z[3] →^* z[4])∧(x[3] →^* x[4])∧(y[3] →^* y[4])∧(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)) →^* TRUE))

(4) -> (1), if ((-@z(y[4], 1@z) →^* y[1])∧(z[4] →^* z[1])∧(x[4] →^* x[1]))

(5) -> (1), if ((y[5] →^* y[1])∧(z[5] →^* z[1])∧(-@z(x[5], 1@z) →^* x[1]))

Cond_eval1(TRUE, x0, x1, x2)
Cond_eval(TRUE, x0, x1, x2)
Cond_eval2(TRUE, x0, x1, x2)
eval(x0, x1, x2)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDPNonInfProof

            ↳ IDP

              ↳ IDependencyGraphProof

                ↳ IDP

                  ↳ IDPNonInfProof

z

(1) -> (5), if ((z[1] →^* z[5])∧(x[1] →^* x[5])∧(y[1] →^* y[5])∧(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)) →^* TRUE))

(4) -> (3), if ((-@z(y[4], 1@z) →^* y[3])∧(z[4] →^* z[3])∧(x[4] →^* x[3]))

(5) -> (3), if ((y[5] →^* y[3])∧(z[5] →^* z[3])∧(-@z(x[5], 1@z) →^* x[3]))

(3) -> (4), if ((z[3] →^* z[4])∧(x[3] →^* x[4])∧(y[3] →^* y[4])∧(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)) →^* TRUE))

(4) -> (1), if ((-@z(y[4], 1@z) →^* y[1])∧(z[4] →^* z[1])∧(x[4] →^* x[1]))

(5) -> (1), if ((y[5] →^* y[1])∧(z[5] →^* z[1])∧(-@z(x[5], 1@z) →^* x[1]))

Cond_eval1(TRUE, x0, x1, x2)
Cond_eval(TRUE, x0, x1, x2)
Cond_eval2(TRUE, x0, x1, x2)
eval(x0, x1, x2)

• We consider the chain EVAL(x[1], y[1], z[1]) → COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1]) which results in the following constraint:
  

  (1)    (EVAL(x[1], y[1], z[1])≥NonInfC∧EVAL(x[1], y[1], z[1])≥COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1])∧(U^Increasing(COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1])), ≥))

  
  
  We simplified constraint (1) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (2)    ((U^Increasing(COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1])), ≥)∧0 ≥ 0∧1 ≥ 0)

  
  
  We simplified constraint (2) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (3)    ((U^Increasing(COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1])), ≥)∧0 ≥ 0∧1 ≥ 0)

  
  
  We simplified constraint (3) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (4)    (1 ≥ 0∧0 ≥ 0∧(U^Increasing(COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1])), ≥))

  
  
  We simplified constraint (4) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (5)    (0 = 0∧0 = 0∧1 ≥ 0∧0 = 0∧0 = 0∧0 ≥ 0∧0 = 0∧(U^Increasing(COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1])), ≥)∧0 = 0)

  
  
  

• We consider the chain EVAL(x[3], y[3], z[3]) → COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3]), COND_EVAL2(TRUE, x[4], y[4], z[4]) → EVAL(x[4], -@z(y[4], 1@z), z[4]), EVAL(x[3], y[3], z[3]) → COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3]) which results in the following constraint:
  

  (6)    (z[4]=z[3]1∧z[3]=z[4]∧-@z(y[4], 1@z)=y[3]1∧&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z))=TRUE∧y[3]=y[4]∧x[3]=x[4]∧x[4]=x[3]1 ⇒ COND_EVAL2(TRUE, x[4], y[4], z[4])≥NonInfC∧COND_EVAL2(TRUE, x[4], y[4], z[4])≥EVAL(x[4], -@z(y[4], 1@z), z[4])∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥))

  
  
  We simplified constraint (6) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (7)    (>@z(y[3], 0@z)=TRUE∧>=@z(0@z, x[3])=TRUE∧>@z(+@z(x[3], y[3]), z[3])=TRUE∧>=@z(z[3], 0@z)=TRUE ⇒ COND_EVAL2(TRUE, x[3], y[3], z[3])≥NonInfC∧COND_EVAL2(TRUE, x[3], y[3], z[3])≥EVAL(x[3], -@z(y[3], 1@z), z[3])∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥))

  
  
  We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (8)    (-1 + y[3] ≥ 0∧(-1)x[3] ≥ 0∧-1 + x[3] + y[3] + (-1)z[3] ≥ 0∧z[3] ≥ 0 ⇒ (U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (9)    (-1 + y[3] ≥ 0∧(-1)x[3] ≥ 0∧-1 + x[3] + y[3] + (-1)z[3] ≥ 0∧z[3] ≥ 0 ⇒ (U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (10)    (-1 + y[3] ≥ 0∧-1 + x[3] + y[3] + (-1)z[3] ≥ 0∧(-1)x[3] ≥ 0∧z[3] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥)∧0 ≥ 0)

  
  
  We simplified constraint (10) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (11)    (-1 + y[3] ≥ 0∧-1 + (-1)x[3] + y[3] + (-1)z[3] ≥ 0∧x[3] ≥ 0∧z[3] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥)∧0 ≥ 0)

  
  
  We simplified constraint (11) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (12)    (x[3] + z[3] + y[3] ≥ 0∧y[3] ≥ 0∧x[3] ≥ 0∧z[3] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥)∧0 ≥ 0)

  
  
  
• We consider the chain EVAL(x[3], y[3], z[3]) → COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3]), COND_EVAL2(TRUE, x[4], y[4], z[4]) → EVAL(x[4], -@z(y[4], 1@z), z[4]), EVAL(x[1], y[1], z[1]) → COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1]) which results in the following constraint:
  

  (13)    (z[3]=z[4]∧&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z))=TRUE∧y[3]=y[4]∧z[4]=z[1]∧x[3]=x[4]∧-@z(y[4], 1@z)=y[1]∧x[4]=x[1] ⇒ COND_EVAL2(TRUE, x[4], y[4], z[4])≥NonInfC∧COND_EVAL2(TRUE, x[4], y[4], z[4])≥EVAL(x[4], -@z(y[4], 1@z), z[4])∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥))

  
  
  We simplified constraint (13) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (14)    (>@z(y[3], 0@z)=TRUE∧>=@z(0@z, x[3])=TRUE∧>@z(+@z(x[3], y[3]), z[3])=TRUE∧>=@z(z[3], 0@z)=TRUE ⇒ COND_EVAL2(TRUE, x[3], y[3], z[3])≥NonInfC∧COND_EVAL2(TRUE, x[3], y[3], z[3])≥EVAL(x[3], -@z(y[3], 1@z), z[3])∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥))

  
  
  We simplified constraint (14) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (15)    (-1 + y[3] ≥ 0∧(-1)x[3] ≥ 0∧-1 + x[3] + y[3] + (-1)z[3] ≥ 0∧z[3] ≥ 0 ⇒ (U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (15) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (16)    (-1 + y[3] ≥ 0∧(-1)x[3] ≥ 0∧-1 + x[3] + y[3] + (-1)z[3] ≥ 0∧z[3] ≥ 0 ⇒ (U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (16) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (17)    ((-1)x[3] ≥ 0∧-1 + x[3] + y[3] + (-1)z[3] ≥ 0∧-1 + y[3] ≥ 0∧z[3] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥))

  
  
  We simplified constraint (17) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (18)    (x[3] ≥ 0∧-1 + (-1)x[3] + y[3] + (-1)z[3] ≥ 0∧-1 + y[3] ≥ 0∧z[3] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥))

  
  
  We simplified constraint (18) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (19)    (x[3] ≥ 0∧y[3] ≥ 0∧x[3] + z[3] + y[3] ≥ 0∧z[3] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥))

  
  
  

• We consider the chain EVAL(x[3], y[3], z[3]) → COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3]) which results in the following constraint:
  

  (20)    (EVAL(x[3], y[3], z[3])≥NonInfC∧EVAL(x[3], y[3], z[3])≥COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])∧(U^Increasing(COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥))

  
  
  We simplified constraint (20) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (21)    ((U^Increasing(COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (21) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (22)    ((U^Increasing(COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (22) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (23)    ((U^Increasing(COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (23) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (24)    (0 = 0∧0 ≥ 0∧(U^Increasing(COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 ≥ 0∧0 = 0)

  
  
  

• We consider the chain EVAL(x[1], y[1], z[1]) → COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1]), COND_EVAL1(TRUE, x[5], y[5], z[5]) → EVAL(-@z(x[5], 1@z), y[5], z[5]), EVAL(x[1], y[1], z[1]) → COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1]) which results in the following constraint:
  

  (25)    (z[5]=z[1]1∧z[1]=z[5]∧y[5]=y[1]1∧&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z))=TRUE∧-@z(x[5], 1@z)=x[1]1∧x[1]=x[5]∧y[1]=y[5] ⇒ COND_EVAL1(TRUE, x[5], y[5], z[5])≥NonInfC∧COND_EVAL1(TRUE, x[5], y[5], z[5])≥EVAL(-@z(x[5], 1@z), y[5], z[5])∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥))

  
  
  We simplified constraint (25) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (26)    (>@z(x[1], 0@z)=TRUE∧>@z(+@z(x[1], y[1]), z[1])=TRUE∧>=@z(z[1], 0@z)=TRUE ⇒ COND_EVAL1(TRUE, x[1], y[1], z[1])≥NonInfC∧COND_EVAL1(TRUE, x[1], y[1], z[1])≥EVAL(-@z(x[1], 1@z), y[1], z[1])∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥))

  
  
  We simplified constraint (26) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (27)    (x[1] + -1 ≥ 0∧x[1] + -1 + y[1] + (-1)z[1] ≥ 0∧z[1] ≥ 0 ⇒ (U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧-2 + (-1)Bound + (-1)z[1] + y[1] + x[1] ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (27) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (28)    (x[1] + -1 ≥ 0∧x[1] + -1 + y[1] + (-1)z[1] ≥ 0∧z[1] ≥ 0 ⇒ (U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧-2 + (-1)Bound + (-1)z[1] + y[1] + x[1] ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (28) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (29)    (z[1] ≥ 0∧x[1] + -1 + y[1] + (-1)z[1] ≥ 0∧x[1] + -1 ≥ 0 ⇒ (U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0∧-2 + (-1)Bound + (-1)z[1] + y[1] + x[1] ≥ 0)

  
  
  We simplified constraint (29) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (30)    (z[1] ≥ 0∧x[1] + y[1] + (-1)z[1] ≥ 0∧x[1] ≥ 0 ⇒ (U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0∧-1 + (-1)Bound + (-1)z[1] + y[1] + x[1] ≥ 0)

  
  
  We simplified constraint (30) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (31)    (z[1] ≥ 0∧x[1] + y[1] + (-1)z[1] ≥ 0∧x[1] ≥ 0∧y[1] ≥ 0 ⇒ (U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0∧-1 + (-1)Bound + (-1)z[1] + y[1] + x[1] ≥ 0)

  
  

  (32)    (z[1] ≥ 0∧x[1] + (-1)y[1] + (-1)z[1] ≥ 0∧x[1] ≥ 0∧y[1] ≥ 0 ⇒ (U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0∧-1 + (-1)Bound + (-1)z[1] + (-1)y[1] + x[1] ≥ 0)

  
  
  We simplified constraint (32) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (33)    (z[1] ≥ 0∧x[1] ≥ 0∧y[1] + z[1] + x[1] ≥ 0∧y[1] ≥ 0 ⇒ (U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0∧-1 + (-1)Bound + x[1] ≥ 0)

  
  
  
• We consider the chain EVAL(x[1], y[1], z[1]) → COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1]), COND_EVAL1(TRUE, x[5], y[5], z[5]) → EVAL(-@z(x[5], 1@z), y[5], z[5]), EVAL(x[3], y[3], z[3]) → COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3]) which results in the following constraint:
  

  (34)    (-@z(x[5], 1@z)=x[3]∧y[5]=y[3]∧z[1]=z[5]∧z[5]=z[3]∧&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z))=TRUE∧x[1]=x[5]∧y[1]=y[5] ⇒ COND_EVAL1(TRUE, x[5], y[5], z[5])≥NonInfC∧COND_EVAL1(TRUE, x[5], y[5], z[5])≥EVAL(-@z(x[5], 1@z), y[5], z[5])∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥))

  
  
  We simplified constraint (34) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (35)    (>@z(x[1], 0@z)=TRUE∧>@z(+@z(x[1], y[1]), z[1])=TRUE∧>=@z(z[1], 0@z)=TRUE ⇒ COND_EVAL1(TRUE, x[1], y[1], z[1])≥NonInfC∧COND_EVAL1(TRUE, x[1], y[1], z[1])≥EVAL(-@z(x[1], 1@z), y[1], z[1])∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥))

  
  
  We simplified constraint (35) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (36)    (x[1] + -1 ≥ 0∧x[1] + -1 + y[1] + (-1)z[1] ≥ 0∧z[1] ≥ 0 ⇒ (U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧-2 + (-1)Bound + (-1)z[1] + y[1] + x[1] ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (36) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (37)    (x[1] + -1 ≥ 0∧x[1] + -1 + y[1] + (-1)z[1] ≥ 0∧z[1] ≥ 0 ⇒ (U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧-2 + (-1)Bound + (-1)z[1] + y[1] + x[1] ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (37) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (38)    (z[1] ≥ 0∧x[1] + -1 + y[1] + (-1)z[1] ≥ 0∧x[1] + -1 ≥ 0 ⇒ 0 ≥ 0∧-2 + (-1)Bound + (-1)z[1] + y[1] + x[1] ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥))

  
  
  We simplified constraint (38) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (39)    (z[1] ≥ 0∧x[1] ≥ 0∧(-1)y[1] + z[1] + x[1] ≥ 0 ⇒ 0 ≥ 0∧-1 + (-1)Bound + x[1] ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥))

  
  
  We simplified constraint (39) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (40)    (z[1] ≥ 0∧x[1] ≥ 0∧(-1)y[1] + z[1] + x[1] ≥ 0∧y[1] ≥ 0 ⇒ 0 ≥ 0∧-1 + (-1)Bound + x[1] ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥))

  
  

  (41)    (z[1] ≥ 0∧x[1] ≥ 0∧y[1] + z[1] + x[1] ≥ 0∧y[1] ≥ 0 ⇒ 0 ≥ 0∧-1 + (-1)Bound + x[1] ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥))

  
  
  

• EVAL(x[1], y[1], z[1]) → COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1])
  
  • (0 = 0∧0 = 0∧1 ≥ 0∧0 = 0∧0 = 0∧0 ≥ 0∧0 = 0∧(U^Increasing(COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1])), ≥)∧0 = 0)
    
  
  
• COND_EVAL2(TRUE, x[4], y[4], z[4]) → EVAL(x[4], -@z(y[4], 1@z), z[4])
  
  • (x[3] + z[3] + y[3] ≥ 0∧y[3] ≥ 0∧x[3] ≥ 0∧z[3] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥)∧0 ≥ 0)
    
  • (x[3] ≥ 0∧y[3] ≥ 0∧x[3] + z[3] + y[3] ≥ 0∧z[3] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥))
    
  
  
• EVAL(x[3], y[3], z[3]) → COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])
  
  • (0 = 0∧0 ≥ 0∧(U^Increasing(COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 ≥ 0∧0 = 0)
    
  
  
• COND_EVAL1(TRUE, x[5], y[5], z[5]) → EVAL(-@z(x[5], 1@z), y[5], z[5])
  
  • (z[1] ≥ 0∧x[1] + y[1] + (-1)z[1] ≥ 0∧x[1] ≥ 0∧y[1] ≥ 0 ⇒ (U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0∧-1 + (-1)Bound + (-1)z[1] + y[1] + x[1] ≥ 0)
    
  • (z[1] ≥ 0∧x[1] ≥ 0∧y[1] + z[1] + x[1] ≥ 0∧y[1] ≥ 0 ⇒ (U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧0 ≥ 0∧-1 + (-1)Bound + x[1] ≥ 0)
    
  • (z[1] ≥ 0∧x[1] ≥ 0∧(-1)y[1] + z[1] + x[1] ≥ 0∧y[1] ≥ 0 ⇒ 0 ≥ 0∧-1 + (-1)Bound + x[1] ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥))
    
  • (z[1] ≥ 0∧x[1] ≥ 0∧y[1] + z[1] + x[1] ≥ 0∧y[1] ≥ 0 ⇒ 0 ≥ 0∧-1 + (-1)Bound + x[1] ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥))
    
  
  

POL(-@z(x₁, x₂)) = x₁ + (-1)x₂   
POL(COND_EVAL2(x₁, x₂, x₃, x₄)) = -1 + (-1)x₄ + x₃ + x₂ + (-1)x₁   
POL(0@z) = 0   
POL(TRUE) = 1   
POL(&&(x₁, x₂)) = 1   
POL(EVAL(x₁, x₂, x₃)) = -1 + (-1)x₃ + x₂ + x₁   
POL(FALSE) = 1   
POL(>@z(x₁, x₂)) = -1   
POL(>=@z(x₁, x₂)) = -1   
POL(COND_EVAL1(x₁, x₂, x₃, x₄)) = -1 + (-1)x₄ + x₃ + x₂ + (-1)x₁   
POL(+@z(x₁, x₂)) = x₁ + x₂   
POL(1@z) = 1   
POL(undefined) = -1   

EVAL(x[3], y[3], z[3]) → COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3])

COND_EVAL1(TRUE, x[5], y[5], z[5]) → EVAL(-@z(x[5], 1@z), y[5], z[5])

EVAL(x[1], y[1], z[1]) → COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1])
COND_EVAL2(TRUE, x[4], y[4], z[4]) → EVAL(x[4], -@z(y[4], 1@z), z[4])
COND_EVAL1(TRUE, x[5], y[5], z[5]) → EVAL(-@z(x[5], 1@z), y[5], z[5])

FALSE¹ → &&(FALSE, FALSE)¹
-@z¹ ↔
TRUE¹ → &&(TRUE, TRUE)¹
&&(FALSE, TRUE)¹ ↔ FALSE¹
FALSE¹ → &&(TRUE, FALSE)¹

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDPNonInfProof

            ↳ IDP

              ↳ IDependencyGraphProof

                ↳ IDP

                  ↳ IDPNonInfProof

                    ↳ AND

                      ↳ IDP

                        ↳ IDependencyGraphProof

                      ↳ IDP

z

(1) -> (5), if ((z[1] →^* z[5])∧(x[1] →^* x[5])∧(y[1] →^* y[5])∧(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)) →^* TRUE))

(4) -> (1), if ((-@z(y[4], 1@z) →^* y[1])∧(z[4] →^* z[1])∧(x[4] →^* x[1]))

(5) -> (1), if ((y[5] →^* y[1])∧(z[5] →^* z[1])∧(-@z(x[5], 1@z) →^* x[1]))

Cond_eval1(TRUE, x0, x1, x2)
Cond_eval(TRUE, x0, x1, x2)
Cond_eval2(TRUE, x0, x1, x2)
eval(x0, x1, x2)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDPNonInfProof

            ↳ IDP

              ↳ IDependencyGraphProof

                ↳ IDP

                  ↳ IDPNonInfProof

                    ↳ AND

                      ↳ IDP

                        ↳ IDependencyGraphProof

                          ↳ IDP

                            ↳ IDPNonInfProof

                      ↳ IDP

z

(1) -> (5), if ((z[1] →^* z[5])∧(x[1] →^* x[5])∧(y[1] →^* y[5])∧(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)) →^* TRUE))

(5) -> (1), if ((y[5] →^* y[1])∧(z[5] →^* z[1])∧(-@z(x[5], 1@z) →^* x[1]))

Cond_eval1(TRUE, x0, x1, x2)
Cond_eval(TRUE, x0, x1, x2)
Cond_eval2(TRUE, x0, x1, x2)
eval(x0, x1, x2)

• We consider the chain EVAL(x[1], y[1], z[1]) → COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1]) which results in the following constraint:
  

  (1)    (EVAL(x[1], y[1], z[1])≥NonInfC∧EVAL(x[1], y[1], z[1])≥COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1])∧(U^Increasing(COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1])), ≥))

  
  
  We simplified constraint (1) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (2)    ((U^Increasing(COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (2) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (3)    ((U^Increasing(COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (3) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (4)    (0 ≥ 0∧0 ≥ 0∧(U^Increasing(COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1])), ≥))

  
  
  We simplified constraint (4) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (5)    (0 = 0∧0 ≥ 0∧0 = 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧(U^Increasing(COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1])), ≥))

  
  
  

• We consider the chain EVAL(x[1], y[1], z[1]) → COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1]), COND_EVAL1(TRUE, x[5], y[5], z[5]) → EVAL(-@z(x[5], 1@z), y[5], z[5]), EVAL(x[1], y[1], z[1]) → COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1]) which results in the following constraint:
  

  (6)    (z[5]=z[1]1∧z[1]=z[5]∧y[5]=y[1]1∧&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z))=TRUE∧-@z(x[5], 1@z)=x[1]1∧x[1]=x[5]∧y[1]=y[5] ⇒ COND_EVAL1(TRUE, x[5], y[5], z[5])≥NonInfC∧COND_EVAL1(TRUE, x[5], y[5], z[5])≥EVAL(-@z(x[5], 1@z), y[5], z[5])∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥))

  
  
  We simplified constraint (6) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (7)    (>@z(x[1], 0@z)=TRUE∧>@z(+@z(x[1], y[1]), z[1])=TRUE∧>=@z(z[1], 0@z)=TRUE ⇒ COND_EVAL1(TRUE, x[1], y[1], z[1])≥NonInfC∧COND_EVAL1(TRUE, x[1], y[1], z[1])≥EVAL(-@z(x[1], 1@z), y[1], z[1])∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥))

  
  
  We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (8)    (x[1] + -1 ≥ 0∧x[1] + -1 + y[1] + (-1)z[1] ≥ 0∧z[1] ≥ 0 ⇒ (U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧-1 + (-1)Bound + (-1)z[1] + y[1] + (2)x[1] ≥ 0∧1 ≥ 0)

  
  
  We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (9)    (x[1] + -1 ≥ 0∧x[1] + -1 + y[1] + (-1)z[1] ≥ 0∧z[1] ≥ 0 ⇒ (U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧-1 + (-1)Bound + (-1)z[1] + y[1] + (2)x[1] ≥ 0∧1 ≥ 0)

  
  
  We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (10)    (x[1] + -1 ≥ 0∧z[1] ≥ 0∧x[1] + -1 + y[1] + (-1)z[1] ≥ 0 ⇒ 1 ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧-1 + (-1)Bound + (-1)z[1] + y[1] + (2)x[1] ≥ 0)

  
  
  We simplified constraint (10) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (11)    (x[1] ≥ 0∧z[1] ≥ 0∧x[1] + y[1] + (-1)z[1] ≥ 0 ⇒ 1 ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧1 + (-1)Bound + (-1)z[1] + y[1] + (2)x[1] ≥ 0)

  
  
  We simplified constraint (11) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (12)    (x[1] ≥ 0∧z[1] ≥ 0∧x[1] + y[1] + (-1)z[1] ≥ 0∧y[1] ≥ 0 ⇒ 1 ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧1 + (-1)Bound + (-1)z[1] + y[1] + (2)x[1] ≥ 0)

  
  

  (13)    (x[1] ≥ 0∧z[1] ≥ 0∧x[1] + (-1)y[1] + (-1)z[1] ≥ 0∧y[1] ≥ 0 ⇒ 1 ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧1 + (-1)Bound + (-1)z[1] + (-1)y[1] + (2)x[1] ≥ 0)

  
  
  We simplified constraint (13) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (14)    (y[1] + z[1] + x[1] ≥ 0∧z[1] ≥ 0∧x[1] ≥ 0∧y[1] ≥ 0 ⇒ 1 ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧1 + (-1)Bound + z[1] + y[1] + (2)x[1] ≥ 0)

  
  
  

• EVAL(x[1], y[1], z[1]) → COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1])
  
  • (0 = 0∧0 ≥ 0∧0 = 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧(U^Increasing(COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1])), ≥))
    
  
  
• COND_EVAL1(TRUE, x[5], y[5], z[5]) → EVAL(-@z(x[5], 1@z), y[5], z[5])
  
  • (x[1] ≥ 0∧z[1] ≥ 0∧x[1] + y[1] + (-1)z[1] ≥ 0∧y[1] ≥ 0 ⇒ 1 ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧1 + (-1)Bound + (-1)z[1] + y[1] + (2)x[1] ≥ 0)
    
  • (y[1] + z[1] + x[1] ≥ 0∧z[1] ≥ 0∧x[1] ≥ 0∧y[1] ≥ 0 ⇒ 1 ≥ 0∧(U^Increasing(EVAL(-@z(x[5], 1@z), y[5], z[5])), ≥)∧1 + (-1)Bound + z[1] + y[1] + (2)x[1] ≥ 0)
    
  
  

POL(-@z(x₁, x₂)) = x₁ + (-1)x₂   
POL(>=@z(x₁, x₂)) = -1   
POL(0@z) = 0   
POL(COND_EVAL1(x₁, x₂, x₃, x₄)) = -1 + (-1)x₄ + x₃ + (2)x₂ + (-1)x₁   
POL(TRUE) = 0   
POL(&&(x₁, x₂)) = 0   
POL(+@z(x₁, x₂)) = x₁ + x₂   
POL(EVAL(x₁, x₂, x₃)) = -1 + (-1)x₃ + x₂ + (2)x₁   
POL(FALSE) = 0   
POL(1@z) = 1   
POL(undefined) = -1   
POL(>@z(x₁, x₂)) = -1   

COND_EVAL1(TRUE, x[5], y[5], z[5]) → EVAL(-@z(x[5], 1@z), y[5], z[5])

COND_EVAL1(TRUE, x[5], y[5], z[5]) → EVAL(-@z(x[5], 1@z), y[5], z[5])

EVAL(x[1], y[1], z[1]) → COND_EVAL1(&&(&&(>@z(+@z(x[1], y[1]), z[1]), >=@z(z[1], 0@z)), >@z(x[1], 0@z)), x[1], y[1], z[1])

&&(FALSE, FALSE)¹ ↔ FALSE¹
-@z¹ ↔
&&(TRUE, TRUE)¹ ↔ TRUE¹
&&(TRUE, FALSE)¹ ↔ FALSE¹
&&(FALSE, TRUE)¹ ↔ FALSE¹

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDPNonInfProof

            ↳ IDP

              ↳ IDependencyGraphProof

                ↳ IDP

                  ↳ IDPNonInfProof

                    ↳ AND

                      ↳ IDP

                        ↳ IDependencyGraphProof

                          ↳ IDP

                            ↳ IDPNonInfProof

                              ↳ IDP

                                ↳ IDependencyGraphProof

                      ↳ IDP

z

Cond_eval1(TRUE, x0, x1, x2)
Cond_eval(TRUE, x0, x1, x2)
Cond_eval2(TRUE, x0, x1, x2)
eval(x0, x1, x2)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDPNonInfProof

            ↳ IDP

              ↳ IDependencyGraphProof

                ↳ IDP

                  ↳ IDPNonInfProof

                    ↳ AND

                      ↳ IDP

                      ↳ IDP

                        ↳ IDependencyGraphProof

z

(4) -> (3), if ((-@z(y[4], 1@z) →^* y[3])∧(z[4] →^* z[3])∧(x[4] →^* x[3]))

(3) -> (4), if ((z[3] →^* z[4])∧(x[3] →^* x[4])∧(y[3] →^* y[4])∧(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)) →^* TRUE))

(4) -> (1), if ((-@z(y[4], 1@z) →^* y[1])∧(z[4] →^* z[1])∧(x[4] →^* x[1]))

Cond_eval1(TRUE, x0, x1, x2)
Cond_eval(TRUE, x0, x1, x2)
Cond_eval2(TRUE, x0, x1, x2)
eval(x0, x1, x2)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDPNonInfProof

            ↳ IDP

              ↳ IDependencyGraphProof

                ↳ IDP

                  ↳ IDPNonInfProof

                    ↳ AND

                      ↳ IDP

                      ↳ IDP

                        ↳ IDependencyGraphProof

                          ↳ IDP

                            ↳ IDPNonInfProof

z

(4) -> (3), if ((-@z(y[4], 1@z) →^* y[3])∧(z[4] →^* z[3])∧(x[4] →^* x[3]))

(3) -> (4), if ((z[3] →^* z[4])∧(x[3] →^* x[4])∧(y[3] →^* y[4])∧(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)) →^* TRUE))

Cond_eval1(TRUE, x0, x1, x2)
Cond_eval(TRUE, x0, x1, x2)
Cond_eval2(TRUE, x0, x1, x2)
eval(x0, x1, x2)

• We consider the chain EVAL(x[3], y[3], z[3]) → COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3]), COND_EVAL2(TRUE, x[4], y[4], z[4]) → EVAL(x[4], -@z(y[4], 1@z), z[4]), EVAL(x[3], y[3], z[3]) → COND_EVAL2(&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z)), x[3], y[3], z[3]) which results in the following constraint:
  

  (1)    (z[4]=z[3]1∧z[3]=z[4]∧-@z(y[4], 1@z)=y[3]1∧&&(&&(&&(>@z(+@z(x[3], y[3]), z[3]), >=@z(z[3], 0@z)), >=@z(0@z, x[3])), >@z(y[3], 0@z))=TRUE∧y[3]=y[4]∧x[3]=x[4]∧x[4]=x[3]1 ⇒ COND_EVAL2(TRUE, x[4], y[4], z[4])≥NonInfC∧COND_EVAL2(TRUE, x[4], y[4], z[4])≥EVAL(x[4], -@z(y[4], 1@z), z[4])∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥))

  
  
  We simplified constraint (1) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (2)    (>@z(y[3], 0@z)=TRUE∧>=@z(0@z, x[3])=TRUE∧>@z(+@z(x[3], y[3]), z[3])=TRUE∧>=@z(z[3], 0@z)=TRUE ⇒ COND_EVAL2(TRUE, x[3], y[3], z[3])≥NonInfC∧COND_EVAL2(TRUE, x[3], y[3], z[3])≥EVAL(x[3], -@z(y[3], 1@z), z[3])∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥))

  
  
  We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (3)    (-1 + y[3] ≥ 0∧(-1)x[3] ≥ 0∧-1 + x[3] + y[3] + (-1)z[3] ≥ 0∧z[3] ≥ 0 ⇒ (U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥)∧(-1)Bound + (-1)z[3] + y[3] + x[3] ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (4)    (-1 + y[3] ≥ 0∧(-1)x[3] ≥ 0∧-1 + x[3] + y[3] + (-1)z[3] ≥ 0∧z[3] ≥ 0 ⇒ (U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥)∧(-1)Bound + (-1)z[3] + y[3] + x[3] ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (5)    (z[3] ≥ 0∧-1 + x[3] + y[3] + (-1)z[3] ≥ 0∧(-1)x[3] ≥ 0∧-1 + y[3] ≥ 0 ⇒ (-1)Bound + (-1)z[3] + y[3] + x[3] ≥ 0∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥)∧0 ≥ 0)

  
  
  We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (6)    (z[3] ≥ 0∧-1 + (-1)x[3] + y[3] + (-1)z[3] ≥ 0∧x[3] ≥ 0∧-1 + y[3] ≥ 0 ⇒ (-1)Bound + (-1)z[3] + y[3] + (-1)x[3] ≥ 0∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥)∧0 ≥ 0)

  
  
  We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (7)    (z[3] ≥ 0∧y[3] ≥ 0∧x[3] ≥ 0∧x[3] + z[3] + y[3] ≥ 0 ⇒ 1 + (-1)Bound + y[3] ≥ 0∧(U^Increasing(EVAL(x[4], -@z(y[4], 1@z), z[4])), ≥)∧0 ≥ 0)